Motivated by security applications where the initial state of a system needs to be kept secret (opaque) to outside observers (intruders), we formulate, analyze and verify the notion of initial-state opacity in discrete ...